% sail -h
Sail 0.17.1 (sail2 @ 435ffd3d9ff211d7e5a7e1792229b0435389980d)
usage: sail <options> <file1.sail> ... <fileN.sail>

  -o <prefix>                               select output filename prefix
  --dir                                     show current Sail library directory
  -i                                        start interactive interpreter
  --is <filename>                           start interactive interpreter and execute commands in script
  --iout <filename>                         print interpreter output to file
  --interact-custom                         drop to an interactive session after running Sail. Differs from -i in that it does not set up the interpreter in the interactive shell.
  --config <file>                           configuration file
  --fmt                                     format input source code
  --fmt-backup <suffix>                     Create backups of formated files as 'file.suffix'
  --fmt-only <file>                         format only this file
  --fmt-skip <file>                         skip formatting this file
  -D <symbol>                               define a symbol for the preprocessor, as $define does in the source code
  --no-warn                                 do not print warnings
  --strict-var                              require var expressions for variable declarations
  --plugin <file>                           load a Sail plugin
  --just-check                              terminate immediately after typechecking
  --memo-z3                                 memoize calls to z3, improving performance when typechecking repeatedly
  --no-memo-z3                              do not memoize calls to z3 (default)
  --have-feature <symbol>                   check if a feature symbol is set by default
  --no-color                                do not use terminal color codes in output
  --string-literal-type                     use a separate string_literal type for string literals
  --undefined-gen                           generate undefined_type functions for types in the specification
  --grouped-regstate                        group registers with same type together in generated register state record
  --non-lexical-flow                        allow non-lexical flow typing
  --no-lexp-bounds-check                    turn off bounds checking for vector assignments in l-expressions
  --auto-mono                               automatically infer how to monomorphise code
  --mono-rewrites                           turn on rewrites for combining bitvector operations
  --mono-split <filename>:<line>:<variable> manually gives a case split for monomorphisation
  --splice <filename>                       add functions from file, replacing existing definitions where necessary
  --smt-solver <solver>                     choose SMT solver. Supported solvers are z3 (default), alt-ergo, cvc4, mathsat, vampire and yices.
  --smt-linearize                           (experimental) force linearization for constraints involving exponentials
  --Oconstant-fold                          apply constant folding optimizations
  --Oaarch64-fast                           apply ARMv8.5 specific optimizations (potentially unsound in general)
  --Ofast-undefined                         turn on fast-undefined mode
  --const-prop-mutrec                       unroll function in a set of mutually recursive functions
  --ddump-initial-ast                       (debug) dump the initial ast to stdout
  --ddump-tc-ast                            (debug) dump the typechecked ast to stdout
  --dtc-verbose <verbosity>                 (debug) verbose typechecker output: 0 is silent
  --dsmt-verbose                            (debug) print SMTLIB constraints sent to SMT solver
  --dmagic-hash                             (debug) allow special character # in identifiers
  --dprofile                                (debug) provide basic profiling information for rewriting passes within Sail
  --ddump-rewrite-ast <prefix>              (debug) dump the ast after each rewriting step to <prefix>_<i>.lem
  --dmono-all-split-errors                  (debug) display all case split errors from monomorphisation, rather than one
  --dmono-analysis <verbosity>              (debug) dump information about monomorphisation analysis: 0 silent, 3 max
  --dmono-continue                          (debug) continue despite monomorphisation errors
  --dbacktrace <length>                     (debug) length of backtrace to show when reporting unreachable code
  --infer-effects                           (deprecated) ignored for compatibility with older versions; effects are always inferred now
  -v                                        print version
  --version                                 print version
  --verbose <verbosity>                     produce verbose output
  --explain-all-variables                   explain all type variables in type error messages
  --explain-constraints                     explain constraints in type error messages
  --explain-verbose                         add the maximum amount of explanation to type errors
  -h                                        display this list of options. Also available as -help or --help
  -help                                     display this list of options
  --help                                    display this list of options 

Options for target sail
  --output-sail                 print Sail code after type checking and initial rewriting
  --output-sail-dir <directory> set a directory to output pretty-printed Sail 

Options for target systemverilog
  --sv                            invoke the Sail systemverilog target
  --sv-output-dir <path>          set the output directory for generated SystemVerilog files
  --sv-include <file>             add include directive to generated SystemVerilog file
  --sv-verilate <compile|run>     Invoke verilator on generated output
  --sv-lines                      output `line directives
  --sv-comb                       output an always_comb block instead of initial block
  --sv-inregs                     take register values from inputs
  --sv-outregs                    output register values
  --sv-int-size <n>               set the maximum width for unknown integers
  --sv-bits-size <n>              set the maximum width for bitvectors with unknown width
  --sv-nostrings                  don't emit any strings, instead emit units
  --sv-nopacked                   don't emit packed datastructures
  --sv-padding                    add padding on packed unions
  --sv-unreachable <functionname> Mark function as unreachable.
  --sv-nomem                      don't emit a dynamic memory implementation
  --sv-fun2wires <functionname>   Use input/output ports instead of emitting a function call
  --sv-specialize <n>             Run n specialization passes on Sail Int-kinded type variables

...